es:ES, T:Type, eq:EqDecider(T), v:T, x:Id, e:{e:E| @loc(e)(x:T)} ,
e':{e':E| e loc e'  & (x after e') = v} .
e'e.(x after e') = v & e''[e,e').((x after e'') = v) 

latex

Definitions	True, T, P  Q, A c B, x:A. B(x), e'e.P(e'), e loc e' , state after e, tt, if b then t else f fi , Top, x,y. t(x;y), x. t(x), P  Q, P  Q, P  Q, , t  T, P & Q, EqDecider(T), x:A. B(x), SqStable(P), @i(x:T), x(s), State(ds)
Lemmas	decidable es-le, es-le wf, sq stable from decidable, es-vartype wf, es-le-loc, es-after wf, es-locl wf, decidable assert, decidable functionality, deq property, fpf-single wf3, es-dds wf, es-dds-single, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, fpf-single wf, next-state-relation, event system wf, assert wf, iff wf, bool wf, Id wf, es-loc wf, es-dtype wf, es-E wf